as:( List). a:. ((((null(as)))  (a  as)) & (a'as. a  a')) 

latex

Definitions	xL. P(x), {T}, P  Q, A, S  T, Top, x. t(x), , True, if b then t else f fi , tt, null(as), b, P  Q, P & Q, x:A. B(x), t  T, x:A. B(x), Dec(P), ff, P  Q, P  Q, x(s), False
Lemmas	qle weakening lt qorder, qless transitivity 2 qorder, qle complement qorder, false wf, cons member, decidable qle, qle weakening eq qorder, l all cons, member singleton, top wf, null wf3, l all wf2, l member wf, null wf2, assert wf, qle wf, l all nil, true wf, not wf, int inc rationals, rationals wf